Задача SAT

Дана КНФ $F = \bigwedge\limits_{i=1}^{\ell} C_i$. Требуется определить, является ли она выполнимой. Если $F$ выполнима, обычно требуется предъявить интерпретацию (булев вектор $\vec{b}$), при которой $F|_{\vec{b}} = 1$. Если $F$ — противоречие, требуется предъявить доказательство невыполнимости.

SAT (от англ. satisfiability — выполнимость) является важнейшей NP-полной задачей. Несмотря на теоретическую сложность, для неё разработаны эффективные с практической точки зрения алгоритмы решения (SAT-solvers). Один из основных методов решения задачи SAT, используемый для проверки логической выполнимости формул.